(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
p(0) → 0
p(s(x)) → x
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(x, y) → if(le(x, y), x, y)
if(true, x, y) → 0
if(false, x, y) → s(minus(p(x), y))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, z1) → if(le(z0, z1), z0, z1)
if(true, z0, z1) → 0
if(false, z0, z1) → s(minus(p(z0), z1))
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, z1) → c5(IF(le(z0, z1), z0, z1), LE(z0, z1))
IF(false, z0, z1) → c7(MINUS(p(z0), z1), P(z0))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(z0, z1) → c5(IF(le(z0, z1), z0, z1), LE(z0, z1))
IF(false, z0, z1) → c7(MINUS(p(z0), z1), P(z0))
K tuples:none
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, MINUS, IF
Compound Symbols:
c4, c5, c7
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
MINUS(
z0,
z1) →
c5(
IF(
le(
z0,
z1),
z0,
z1),
LE(
z0,
z1)) by
MINUS(0, z0) → c5(IF(true, 0, z0), LE(0, z0))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
MINUS(x0, x1) → c5
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, z1) → if(le(z0, z1), z0, z1)
if(true, z0, z1) → 0
if(false, z0, z1) → s(minus(p(z0), z1))
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
IF(false, z0, z1) → c7(MINUS(p(z0), z1), P(z0))
MINUS(0, z0) → c5(IF(true, 0, z0), LE(0, z0))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
MINUS(x0, x1) → c5
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
IF(false, z0, z1) → c7(MINUS(p(z0), z1), P(z0))
MINUS(0, z0) → c5(IF(true, 0, z0), LE(0, z0))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
MINUS(x0, x1) → c5
K tuples:none
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, IF, MINUS
Compound Symbols:
c4, c7, c5, c5
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
MINUS(0, z0) → c5(IF(true, 0, z0), LE(0, z0))
MINUS(x0, x1) → c5
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, z1) → if(le(z0, z1), z0, z1)
if(true, z0, z1) → 0
if(false, z0, z1) → s(minus(p(z0), z1))
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
IF(false, z0, z1) → c7(MINUS(p(z0), z1), P(z0))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
IF(false, z0, z1) → c7(MINUS(p(z0), z1), P(z0))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
K tuples:none
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, IF, MINUS
Compound Symbols:
c4, c7, c5
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
IF(
false,
z0,
z1) →
c7(
MINUS(
p(
z0),
z1),
P(
z0)) by
IF(false, 0, x1) → c7(MINUS(0, x1), P(0))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
IF(false, x0, x1) → c7
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, z1) → if(le(z0, z1), z0, z1)
if(true, z0, z1) → 0
if(false, z0, z1) → s(minus(p(z0), z1))
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, 0, x1) → c7(MINUS(0, x1), P(0))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
IF(false, x0, x1) → c7
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, 0, x1) → c7(MINUS(0, x1), P(0))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
IF(false, x0, x1) → c7
K tuples:none
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, MINUS, IF
Compound Symbols:
c4, c5, c7, c7
(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
IF(false, 0, x1) → c7(MINUS(0, x1), P(0))
IF(false, x0, x1) → c7
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, z1) → if(le(z0, z1), z0, z1)
if(true, z0, z1) → 0
if(false, z0, z1) → s(minus(p(z0), z1))
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
K tuples:none
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, MINUS, IF
Compound Symbols:
c4, c5, c7
(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
We considered the (Usable) Rules:
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
And the Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(IF(x1, x2, x3)) = [2]x2
POL(LE(x1, x2)) = 0
POL(MINUS(x1, x2)) = [2]x1
POL(P(x1)) = 0
POL(c4(x1)) = x1
POL(c5(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = 0
POL(le(x1, x2)) = [5]x1
POL(s(x1)) = [4] + x1
POL(true) = [2]
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, z1) → if(le(z0, z1), z0, z1)
if(true, z0, z1) → 0
if(false, z0, z1) → s(minus(p(z0), z1))
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
K tuples:
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, MINUS, IF
Compound Symbols:
c4, c5, c7
(13) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, z1) → if(le(z0, z1), z0, z1)
if(true, z0, z1) → 0
if(false, z0, z1) → s(minus(p(z0), z1))
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
S tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
K tuples:
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, MINUS, IF
Compound Symbols:
c4, c5, c7
(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
LE(s(z0), s(z1)) → c4(LE(z0, z1))
We considered the (Usable) Rules:
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
And the Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0) = 0
POL(IF(x1, x2, x3)) = [2]x22
POL(LE(x1, x2)) = [2]x1
POL(MINUS(x1, x2)) = [2] + [2]x1 + [2]x12
POL(P(x1)) = 0
POL(c4(x1)) = x1
POL(c5(x1, x2)) = x1 + x2
POL(c7(x1, x2)) = x1 + x2
POL(false) = 0
POL(le(x1, x2)) = 0
POL(s(x1)) = [1] + x1
POL(true) = 0
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
p(0) → 0
p(s(z0)) → z0
le(0, z0) → true
le(s(z0), 0) → false
le(s(z0), s(z1)) → le(z0, z1)
minus(z0, z1) → if(le(z0, z1), z0, z1)
if(true, z0, z1) → 0
if(false, z0, z1) → s(minus(p(z0), z1))
Tuples:
LE(s(z0), s(z1)) → c4(LE(z0, z1))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
S tuples:none
K tuples:
IF(false, s(z0), x1) → c7(MINUS(z0, x1), P(s(z0)))
MINUS(s(z0), 0) → c5(IF(false, s(z0), 0), LE(s(z0), 0))
MINUS(s(z0), s(z1)) → c5(IF(le(z0, z1), s(z0), s(z1)), LE(s(z0), s(z1)))
LE(s(z0), s(z1)) → c4(LE(z0, z1))
Defined Rule Symbols:
p, le, minus, if
Defined Pair Symbols:
LE, MINUS, IF
Compound Symbols:
c4, c5, c7
(17) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(18) BOUNDS(O(1), O(1))